Nuprl Lemma : st-length-encrypt
0,22
postcript
pdf
T
:(Id
Type),
tab
:secret-table(
T
),
keyv
:((
+Atom1)
data(
T
)).
||encrypt(
tab
;
keyv
)|| = ||
tab
||
latex
Definitions
{
x
:
A
|
B
(
x
) }
,
,
t
T
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
||
tab
||
,
<
a
,
b
>
,
,
s
=
t
,
P
Q
,
False
,
A
,
A
B
,
Type
,
Prop
,
True
,
i
j
,
b
,
b
,
,
a
<
b
,
i
<
j
,
T
,
P
Q
,
x
:
A
B
(
x
)
,
P
&
Q
,
P
Q
,
Unit
,
left
+
right
,
encrypt(
tab
;
keyv
)
,
secret-table(
T
)
,
Id
,
data(
T
)
,
Atom$n
Lemmas
nat
wf
,
data
wf
,
secret-table
wf
,
Id
wf
,
eqtt
to
assert
,
assert
of
lt
int
,
iff
transitivity
,
eqff
to
assert
,
squash
wf
,
true
wf
,
bnot
of
lt
int
,
assert
of
le
int
,
lt
int
wf
,
le
wf
,
bool
wf
,
bnot
wf
,
assert
wf
,
le
int
wf
origin